'''
Modified on Sep 02, 2011

@author: nktran
'''

import re
import os
import sys
from fsa import FSA
from constant import *

class Angluin:
    """
    Implementation of angluin algorithm
    """ 
    def __init__(self, ext=""):
        """
        """
        self.__lamda = ""
        self.__mquery = 0
        self.__cquery = 0
        self.__ext__ = ext
        
        self.table = dict()
        self.prefix = set()
        self.suffix = set()
        self.alphabet = set()
        self.query = dict()
        self.instance = set()        

    def __init_table(self):
        """
        """
        self.prefix.add(self.__lamda)
        self.suffix.add(self.__lamda)
        self.set_alphabet()
        self.set_instance()
        
        ans = self.__get_answer('_lamda_')
        self.__mquery = self.__mquery + 1        
        if ans == 'y':
            self.table[self.__lamda] = {self.__lamda:1}
            self.query[self.__lamda] = 1
        else:
            self.table[self.__lamda] = {self.__lamda:0}
            self.query[self.__lamda] = 0
        
        for a in self.alphabet:
            ans = self.__get_answer(a)
            self.__mquery = self.__mquery + 1
            if ans == 'y':
                self.table[a] = {self.__lamda:1}
                self.query[a] = 1
            else:                
                self.table[a] = {self.__lamda:0}
                self.query[a] = 0        
       
    def set_alphabet(self):
        """
        Initialize alphabet
        """
        fname = ALPHABET_FILE + self.__ext__
        self.alphabet = self.read_file(fname,'\s+')
        print self.alphabet    

    def set_instance(self):
        """
        """
        fname = INSTANCE_FILE + self.__ext__
        self.instance = self.read_file(fname,'\n')
        print self.instance
        
    def read_file(self, fname, delim):
        """
        """
        if fname not in os.listdir("."):
            print fname, 'does not exist!!!'
            sys.exit(1)
            
        result = set()
        fin = open(fname, 'r')
        try:
            lines = re.split(delim, fin.read())
            for line in lines:
                if len(line.strip()) == 0: continue
                result.add(line)
        finally:
            fin.close()
        
        return result

    def __format(self,string):
        """
        Modify string format
        """
        if string == "":
            return "_lamda_"        
        return string    
    
    def __check_closed(self):
        """
        """
        for s in self.prefix:
            for a in self.alphabet:
                flag = False
                for s1 in self.prefix:
                    if self.table.has_key(s+a) and self.table.has_key(s1) and \
                            self.table[s+a] == self.table[s1]:
                        flag = True
                if flag == False:
                    self.__print_file('No row in suffix equals to row ' + s+a)
                    return False
        return True
         
    def __check_consistent(self):
        """
        """
        for s1 in self.prefix:
            for s2 in self.prefix:
                if s1 == s2: continue
                if self.table[s1] == self.table[s2]:
                    for a in self.alphabet:
                        if self.table[s1+a] != self.table[s2+a]:
                            self.__print_file('Row [' + self.__format(s1) + ']= row [' + self.__format(s2) + \
                                               ']. But row [' + s1+a + '] != row [' + s2+a + ']')
                            return False
        return True

    def __add_to_table(self, pre, suf, val):
        """
        """
        
        if self.table.has_key(pre):
            self.table[pre][suf] = val
        else:
            self.table[pre] = {suf:val}

    def __get_answer(self, query):
        """
        """
        if query in self.instance:
            self.__print_query(query, 'yes')
            return 'y'
        
        self.__print_query(query, 'no')
        return 'n'
    
    def __new_query(self, pre, suf):
        """
        """
        ans = self.__get_answer(pre + suf)
        self.__mquery = self.__mquery + 1
        if ans == 'y':
            self.__add_to_table(pre, suf, 1)
            self.query[pre+suf] = 1
        else:
            self.__add_to_table(pre, suf, 0)
            self.query[pre+suf] = 0
        

    def __update_table(self,temp,flag):
        """
        """
        if flag == 0:
            for pre in self.prefix:
                # prefix
                for suf in temp:
                    if not self.query.has_key(pre+suf):
                        self.__new_query(pre,suf)
                    else:
                        self.__add_to_table(pre, suf, self.query[pre+suf])
                # prefix + alphabet
                for a in self.alphabet:
                    for suf in temp:
                        if not self.query.has_key(pre+a+suf):
                            self.__new_query(pre+a, suf)
                        else:
                            self.__add_to_table(pre+a, suf, self.query[pre+a+suf])                   
        else:
            for pre in temp:
                # prefix
                for suf in self.suffix:
                    if not self.query.has_key(pre+suf):
                        self.__new_query(pre, suf)
                    else:
                        self.__add_to_table(pre, suf, self.query[pre+suf])
                # prefix + suffix
                for a in self.alphabet:
                    for suf in self.suffix:
                        if not self.query.has_key(pre+a+suf):
                            self.__new_query(pre+a, suf)
                        else:
                            self.__add_to_table(pre+a, suf, self.query[pre+a+suf])

    def __print_query(self, query, ans):
        """
        """
        fout = open (QUERY_FILE + self.__ext__, 'a')
        try:
            fout.write('query= ' + query)
            fout.write('\t\tin_language = ' + ans)
            fout.write('\n')
        finally:
            fout.close()
    
    def __print_file(self, query):
        """
        """
        fout = open(QUERY_FILE + self.__ext__, 'a')
        try:
            fout.write(query + '\n')
        finally:
            fout.close()
            
    def __print_set(self, string, inSet):
        """
        """
        fout = open(QUERY_FILE + self.__ext__, 'a')
        fout.write(string + ':')
        try:
            for e in inSet:
                fout.write(self.__format(e) + ' ')                
            fout.write('\n')
        finally:
            fout.close()        
    
    def __print_table(self, number):
        """
        """
        fout = open(TABLE_FILE + self.__ext__, 'a')
        try:
            fout.write("# Table " + str(number) + '\n' )
            fout.write("Prefix: {")
            for pre in self.prefix:
                fout.write(self.__format(pre) + ', ')
            fout.write("}")
            fout.write("\n Suffix: {")
            for suf in self.suffix:
                fout.write(self.__format(suf) + ', ')
            fout.write("}\n")                            
            for key in self.table.keys():
                for val in self.table[key].keys():
                    fout.write('T[' + self.__format(key) + '+' + self.__format(val) + ']=T[' + 
                               key + val + ']' +  '=' + str(self.table[key][val]) + '\t  ')
                fout.write('\n')
            fout.write('\n')
        finally:
            fout.close()
        
    def learn(self):
        """
        Induce grammar based on membership query and counterexamples
        """
        self.__init_table()            
        # Loop        
        number = 0
        while True:          
            is_consistent = self.__check_consistent()
            is_closed = self.__check_closed()
            while not is_consistent or not is_closed:
                if not is_consistent:
                    self.__print_file('Table ' + str(number) + ' is not consistent!')
                    print 'Table',str(number),'is not consistent!'
                    
                    temp = list()
                    for pre1 in self.prefix:
                        for pre2 in self.prefix:                        
                            if pre1 != pre2 and self.table[pre1] == self.table[pre2]:
                                for suf in self.suffix:                                
                                    for a in self.alphabet:
                                        if self.table[pre1+a][suf] != self.table[pre2+a][suf] \
                                                and a+suf not in self.suffix:
                                            temp.append(a+suf)
                                            break
                                    if len(temp) > 0: break
                            if len(temp) > 0: break
                        if len(temp) > 0: break                        
                    # end for
                    string = 'Adding {'
                    print 'Adding ',
                    for suf in temp:                        
                        self.suffix.add(suf)
                        print suf,
                        string = string + suf + ', '
                    print ' to the suffix set!'
                    string = string + '} to the suffix set!'                    
                    self.__print_file(string)
                    self.__print_set('prefix', self.prefix)
                    self.__print_set('suffix', self.suffix)                    
                    # update table after adding new elements into suffix set
                    self.__update_table(temp, 0)
                    
                    number = number + 1
                    self.__print_table(number)                    
                                                     
                if not is_closed:
                    print 'Table',str(number),'is not closed!'
                    self.__print_file('Table ' + str(number) + ' is not closed!')
                    
                    temp = list()
                    for pre1 in self.prefix:
                        for a in self.alphabet:
                            if pre1+a in self.prefix:
                                continue
                            flag = True
                            has_key = self.table.has_key(pre1+a)                            
                            for pre in self.prefix:
                                if has_key and self.table[pre1+a] == self.table[pre]:
                                    flag = False
                                    break
                            if flag:
                                temp.append(pre1+a)
                                break
                        if len(temp) > 0:
                            break
                    # end for
                    print 'Adding ',
                    string = 'Adding {'
                    for pre in temp:
                        self.prefix.add(pre)
                        print pre,
                        string = string + pre + ", "
                    print ' to the prefix set!'
                    string = string + '} to the prefix set!'
                    self.__print_file(string)
                    self.__print_set('prefix', self.prefix)
                    self.__print_set('suffix', self.suffix)

                    # Update table after adding new elements into prefix set
                    self.__update_table(temp,1)
                    
                    number = number + 1
                    self.__print_table(number)                                                            
                # end if
                is_consistent = self.__check_consistent()
                is_closed = self.__check_closed()                
            # end membership queries
            print "Table", str(number),"is closed and consistent."
            self.__print_file('#Table ' + str(number) + ' is closed and consistent.')
            
            acceptor = FSA()
            acceptor.construct(self)
            acceptor.toString()
                      
            self.__cquery = self.__cquery + 1
            ans = raw_input("C_Query " + str(self.__cquery) + " : equivalent (y/counterexample)? ")
            if ans == 'y':
                break
            else:
                # Adding new elements into prefix set
                temp = list()
                pre_term = ""
                for substr in re.split('\s+', ans):
                    pre_term = pre_term + substr
                    temp.append(pre_term)
                    
                string = 'Adding {'
                for pre in temp:
                    self.prefix.add(pre)
                    string = string + pre + ', '
                string = string + '} to prefix set!'                
                self.__print_file(string)
                self.__print_set('prefix', self.prefix)
                self.__print_set('suffix', self.suffix)
                #Update table                
                self.__update_table(temp, 1)  
                
                number = number + 1
                self.__print_table(number)                    
                                                                
if __name__ == "__main__":
    alg = Angluin()
    alg.learn()
    